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
for X2 being non empty Subset of
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
for X2 being non empty Subset of
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 ; :: thesis: for X2 being non empty Subset of
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 ; :: 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 : B2 in F2 } ;
set Y1 = { (inf B1) where B1 is Subset of : B1 in F1 } ;
A3: { (inf B2) where B2 is Subset of : B2 in F2 } c= { (inf B1) where B1 is Subset of : B1 in F1 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (inf B2) where B2 is Subset of : B2 in F2 } or x in { (inf B1) where B1 is Subset of : B1 in F1 } )
assume x in { (inf B2) where B2 is Subset of : B2 in F2 } ; :: thesis: x in { (inf B1) where B1 is Subset of : B1 in F1 }
then consider B2 being Subset of 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:4;
then reconsider B1 = B2 as Subset of 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 : B1 in F1 } by A2, A4, A5; :: thesis: verum

end;

{ (inf B1) where B1 is Subset of : B1 in F1 } c= { (inf B2) where B2 is Subset of : B2 in F2 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (inf B1) where B1 is Subset of : B1 in F1 } or x in { (inf B2) where B2 is Subset of : B2 in F2 } )
assume x in { (inf B1) where B1 is Subset of : B1 in F1 } ; :: thesis: x in { (inf B2) where B2 is Subset of : B2 in F2 }
then consider B1 being Subset of 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:4;
then reconsider B2 = B1 as Subset of 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 : B2 in F2 } by A2, A6, A7; :: thesis: verum

end;

then { (inf B1) where B1 is Subset of : B1 in F1 } = { (inf B2) where B2 is Subset of : B2 in F2 } by A3, XBOOLE_0:def 10;
hence lim_inf F1 = lim_inf F2 by A1, YELLOW_0:17, YELLOW_0:26; :: thesis: verum