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 }

hence lim_inf F1 = lim_inf F2 by A1, YELLOW_0:17, YELLOW_0:26; :: thesis: verum

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

{ (inf B1) where B1 is Subset of L1 : B1 in F1 } c= { (inf B2) where B2 is Subset of L2 : B2 in F2 }
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;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

proof

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;
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;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

hence lim_inf F1 = lim_inf F2 by A1, YELLOW_0:17, YELLOW_0:26; :: thesis: verum