let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies for u1 being Vertex of G1

for u2 being Vertex of G2 st u1 = u2 & u1 is simplicial holds

u2 is simplicial )

assume A1: G1 == G2 ; :: thesis: for u1 being Vertex of G1

for u2 being Vertex of G2 st u1 = u2 & u1 is simplicial holds

u2 is simplicial

let u1 be Vertex of G1; :: thesis: for u2 being Vertex of G2 st u1 = u2 & u1 is simplicial holds

u2 is simplicial

let u2 be Vertex of G2; :: thesis: ( u1 = u2 & u1 is simplicial implies u2 is simplicial )

assume A2: u1 = u2 ; :: thesis: ( not u1 is simplicial or u2 is simplicial )

assume A3: u1 is simplicial ; :: thesis: u2 is simplicial

for u2 being Vertex of G2 st u1 = u2 & u1 is simplicial holds

u2 is simplicial )

assume A1: G1 == G2 ; :: thesis: for u1 being Vertex of G1

for u2 being Vertex of G2 st u1 = u2 & u1 is simplicial holds

u2 is simplicial

let u1 be Vertex of G1; :: thesis: for u2 being Vertex of G2 st u1 = u2 & u1 is simplicial holds

u2 is simplicial

let u2 be Vertex of G2; :: thesis: ( u1 = u2 & u1 is simplicial implies u2 is simplicial )

assume A2: u1 = u2 ; :: thesis: ( not u1 is simplicial or u2 is simplicial )

assume A3: u1 is simplicial ; :: thesis: u2 is simplicial

now :: thesis: u2 is simplicial end;

hence
u2 is simplicial
; :: thesis: verumper cases
( G1 .AdjacentSet {u1} = {} or G1 .AdjacentSet {u1} <> {} )
;

end;