let L1, L2 be complete LATTICE; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X1 being non empty Subset of L1
for X2 being non empty Subset of L2
for F1 being Filter of (BoolePoset X1)
for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2 )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: for X1 being non empty Subset of L1
for X2 being non empty Subset of L2
for F1 being Filter of (BoolePoset X1)
for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2
let X1 be non empty Subset of L1; :: thesis: for X2 being non empty Subset of L2
for F1 being Filter of (BoolePoset X1)
for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2
let X2 be non empty Subset of L2; :: thesis: for F1 being Filter of (BoolePoset X1)
for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2
let F1 be Filter of (BoolePoset X1); :: thesis: for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2
let F2 be Filter of (BoolePoset X2); :: thesis: ( F1 = F2 implies lim_inf F1 = lim_inf F2 )
assume A2: F1 = F2 ; :: thesis: lim_inf F1 = lim_inf F2
set Y2 = { (inf B2) where B2 is Subset of L2 : B2 in F2 } ;
set Y1 = { (inf B1) where B1 is Subset of L1 : B1 in F1 } ;
A3: { (inf B2) where B2 is Subset of L2 : B2 in F2 } c= { (inf B1) where B1 is Subset of L1 : B1 in F1 }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } or x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } )
assume x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } ; :: thesis: x in { (inf B1) where B1 is Subset of L1 : B1 in F1 }
then consider B2 being Subset of L2 such that
A4: x = inf B2 and
A5: B2 in F2 ;
F1 c= the carrier of (BoolePoset X1) ;
then F1 c= bool X1 by WAYBEL_7:2;
then reconsider B1 = B2 as Subset of L1 by A2, A5, XBOOLE_1:1;
inf B1 = inf B2 by A1, YELLOW_0:17, YELLOW_0:27;
hence x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } by A2, A4, A5; :: thesis: verum
end;
{ (inf B1) where B1 is Subset of L1 : B1 in F1 } c= { (inf B2) where B2 is Subset of L2 : B2 in F2 }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } or x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } )
assume x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } ; :: thesis: x in { (inf B2) where B2 is Subset of L2 : B2 in F2 }
then consider B1 being Subset of L1 such that
A6: x = inf B1 and
A7: B1 in F1 ;
F2 c= the carrier of (BoolePoset X2) ;
then F2 c= bool X2 by WAYBEL_7:2;
then reconsider B2 = B1 as Subset of L2 by A2, A7, XBOOLE_1:1;
inf B1 = inf B2 by A1, YELLOW_0:17, YELLOW_0:27;
hence x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } by A2, A6, A7; :: thesis: verum
end;
then { (inf B1) where B1 is Subset of L1 : B1 in F1 } = { (inf B2) where B2 is Subset of L2 : B2 in F2 } by A3;
hence lim_inf F1 = lim_inf F2 by A1, YELLOW_0:17, YELLOW_0:26; :: thesis: verum