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;

( 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

( 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 ) )

then A38:
LattRel it1 = LattRel it2
;( ( 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 ) )

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;hereby :: thesis: ( a in LattRel it2 implies a in LattRel it1 )

assume
a in LattRel it2
; :: thesis: a in LattRel it1assume
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;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

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

( 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