let it1, it2 be strict Lattice; :: thesis: ( the carrier of it1 = P & ( for x, y being Element of it1 ex x', y' being Element of L st
( x = x' & y = y' & ( x [= y implies x' [= y' ) & ( x' [= y' implies x [= y ) ) ) & the carrier of it2 = P & ( for x, y being Element of it2 ex x', y' being Element of L st
( x = x' & y = y' & ( x [= y implies x' [= y' ) & ( x' [= y' implies x [= y ) ) ) implies it1 = it2 )
assume that
A18:
( the carrier of it1 = P & ( for x, y being Element of it1 ex x', y' being Element of L st
( x = x' & y = y' & ( x [= y implies x' [= y' ) & ( x' [= y' implies x [= y ) ) ) )
and
A19:
( the carrier of it2 = P & ( for x, y being Element of it2 ex x', y' being Element of L st
( x = x' & y = y' & ( x [= y implies x' [= y' ) & ( x' [= y' implies x [= y ) ) ) )
; :: thesis: it1 = it2
A20:
LattPOSet it1 = RelStr(# the carrier of it1,(LattRel it1) #)
;
A21:
LattPOSet it2 = RelStr(# the carrier of it2,(LattRel it2) #)
;
A22:
LattRel it1 = { [p,q] where p, q is Element of it1 : p [= q }
by FILTER_1:def 8;
A23:
LattRel it2 = { [p,q] where p, q is Element of it2 : p [= q }
by FILTER_1:def 8;
now let a be
set ;
:: 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 it2then consider p1,
q1 being
Element of
it1 such that A24:
(
a = [p1,q1] &
p1 [= q1 )
by A22;
reconsider p1 =
p1,
q1 =
q1 as
Element of
it1 ;
consider pl1,
ql1 being
Element of
L such that A25:
(
p1 = pl1 &
q1 = ql1 & (
p1 [= q1 implies
pl1 [= ql1 ) & (
pl1 [= ql1 implies
p1 [= q1 ) )
by A18;
reconsider p2 =
p1,
q2 =
q1 as
Element of
it2 by A18, A19;
consider pl2,
ql2 being
Element of
L such that A26:
(
p2 = pl2 &
q2 = ql2 & (
p2 [= q2 implies
pl2 [= ql2 ) & (
pl2 [= ql2 implies
p2 [= q2 ) )
by A19;
thus
a in LattRel it2
by A23, A24, A25, A26;
:: thesis: verum
end; assume
a in LattRel it2
;
:: thesis: a in LattRel it1then consider p1,
q1 being
Element of
it2 such that A27:
(
a = [p1,q1] &
p1 [= q1 )
by A23;
reconsider p1 =
p1,
q1 =
q1 as
Element of
it2 ;
consider pl1,
ql1 being
Element of
L such that A28:
(
p1 = pl1 &
q1 = ql1 & (
p1 [= q1 implies
pl1 [= ql1 ) & (
pl1 [= ql1 implies
p1 [= q1 ) )
by A19;
reconsider p2 =
p1,
q2 =
q1 as
Element of
it1 by A18, A19;
consider pl2,
ql2 being
Element of
L such that A29:
(
p2 = pl2 &
q2 = ql2 & (
p2 [= q2 implies
pl2 [= ql2 ) & (
pl2 [= ql2 implies
p2 [= q2 ) )
by A18;
thus
a in LattRel it1
by A22, A27, A28, A29;
:: thesis: verum end;
then
LattRel it1 = LattRel it2
by TARSKI:2;
hence
it1 = it2
by A18, A19, A20, A21, LATTICE3:6; :: thesis: verum