Theorem 4cycl2v2nb

Description: In a (maybe degenerate) 4-cycle, two vertice have two (maybe not different) common neighbors. (Contributed by Alexander van der Vekens, 19-Nov-2017) (Revised by AV, 2-Apr-2021)

	Ref	Expression
Assertion	4cycl2v2nb	|- ( ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) -> ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) )

Proof

Step	Hyp	Ref	Expression
1		prssi	|- ( ( { A , B } e. E /\ { B , C } e. E ) -> { { A , B } , { B , C } } C_ E )
2		prcom	|- { D , A } = { A , D }
3	2	eleq1i	|- ( { D , A } e. E <-> { A , D } e. E )
4	3	biimpi	|- ( { D , A } e. E -> { A , D } e. E )
5		prcom	|- { C , D } = { D , C }
6	5	eleq1i	|- ( { C , D } e. E <-> { D , C } e. E )
7	6	biimpi	|- ( { C , D } e. E -> { D , C } e. E )
8		prssi	|- ( ( { A , D } e. E /\ { D , C } e. E ) -> { { A , D } , { D , C } } C_ E )
9	4 7 8	syl2anr	|- ( ( { C , D } e. E /\ { D , A } e. E ) -> { { A , D } , { D , C } } C_ E )
10	1 9	anim12i	|- ( ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) -> ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) )