let it1, it2 be strict Lattice; :: thesis: ( the carrier of it1 = P & ( for x, y being Element of it1 ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) & the carrier of it2 = P & ( for x, y being Element of it2 ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) implies it1 = it2 )
assume that
A30: the carrier of it1 = P and
A31: for x, y being Element of it1 ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) and
A32: the carrier of it2 = P and
A33: for x, y being Element of it2 ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ; :: thesis: it1 = it2
A34: LattRel it2 = { [p,q] where p, q is Element of it2 : p [= q } by FILTER_1:def 8;
A35: LattRel it1 = { [p,q] where p, q is Element of it1 : p [= q } by FILTER_1:def 8;
now :: thesis: for a being object holds
( ( a in LattRel it1 implies a in LattRel it2 ) & ( a in LattRel it2 implies a in LattRel it1 ) )
let a be object ; :: thesis: ( ( a in LattRel it1 implies a in LattRel it2 ) & ( a in LattRel it2 implies a in LattRel it1 ) )
hereby :: thesis: ( a in LattRel it2 implies a in LattRel it1 )
assume a in LattRel it1 ; :: thesis: a in LattRel it2
then consider p1, q1 being Element of it1 such that
A36: ( a = [p1,q1] & p1 [= q1 ) by A35;
reconsider p1 = p1, q1 = q1 as Element of it1 ;
reconsider p2 = p1, q2 = q1 as Element of it2 by A30, A32;
( ex pl1, ql1 being Element of L st
( p1 = pl1 & q1 = ql1 & ( p1 [= q1 implies pl1 [= ql1 ) & ( pl1 [= ql1 implies p1 [= q1 ) ) & ex pl2, ql2 being Element of L st
( p2 = pl2 & q2 = ql2 & ( p2 [= q2 implies pl2 [= ql2 ) & ( pl2 [= ql2 implies p2 [= q2 ) ) ) by A31, A33;
hence a in LattRel it2 by A34, A36; :: thesis: verum
end;
assume a in LattRel it2 ; :: thesis: a in LattRel it1
then consider p1, q1 being Element of it2 such that
A37: ( a = [p1,q1] & p1 [= q1 ) by A34;
reconsider p1 = p1, q1 = q1 as Element of it2 ;
reconsider p2 = p1, q2 = q1 as Element of it1 by A30, A32;
( ex pl1, ql1 being Element of L st
( p1 = pl1 & q1 = ql1 & ( p1 [= q1 implies pl1 [= ql1 ) & ( pl1 [= ql1 implies p1 [= q1 ) ) & ex pl2, ql2 being Element of L st
( p2 = pl2 & q2 = ql2 & ( p2 [= q2 implies pl2 [= ql2 ) & ( pl2 [= ql2 implies p2 [= q2 ) ) ) by A31, A33;
hence a in LattRel it1 by A35, A37; :: thesis: verum
end;
then A38: LattRel it1 = LattRel it2 ;
( LattPOSet it1 = RelStr(# the carrier of it1,(LattRel it1) #) & LattPOSet it2 = RelStr(# the carrier of it2,(LattRel it2) #) ) ;
hence it1 = it2 by A30, A32, A38, LATTICE3:6; :: thesis: verum