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

now :: thesis: u2 is simplicial

per cases ( G1 .AdjacentSet {u1} = {} or G1 .AdjacentSet {u1} <> {} ) ;

suppose G1 .AdjacentSet {u1} = {} ; :: thesis: u2 is simplicial

then G2 .AdjacentSet {u2} = {} by A1, A2, Th50;
hence u2 is simplicial ; :: thesis: verum

end;

suppose A4: G1 .AdjacentSet {u1} <> {} ; :: thesis: u2 is simplicial

set H1 = the AdjGraph of G1,{u1};
the AdjGraph of G1,{u1} is complete by A3, A4;
then for H2 being AdjGraph of G2,{u2} holds H2 is complete by A1, A2, Th58, Th61;
hence u2 is simplicial ; :: thesis: verum

end;

end;

end;

hence u2 is simplicial ; :: thesis: verum