let R1, R2 be complete LATTICE; :: thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; :: thesis: for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2
let N1 be net of R1; :: thesis: for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2
let N2 be net of R2; :: thesis: ( N1 = N2 implies lim_inf N1 = lim_inf N2 )
assume A2: N1 = N2 ; :: thesis: lim_inf N1 = lim_inf N2
set X1 = { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } ;
set X2 = { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } ;
{ ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } = { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum }

proof

thus { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } c= { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } :: according to XBOOLE_0:def 10 :: thesis: { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } c= { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } or e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } )
assume e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } ; :: thesis: e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum }
then consider j1 being Element of N1 such that
A3: e = "/\" ( { (N1 . i) where i is Element of N1 : i >= j1 } ,R1) ;
reconsider j2 = j1 as Element of N2 by A2;
set Y1 = { (N1 . i) where i is Element of N1 : i >= j1 } ;
set Y2 = { (N2 . i) where i is Element of N2 : i >= j2 } ;
{ (N1 . i) where i is Element of N1 : i >= j1 } = { (N2 . i) where i is Element of N2 : i >= j2 }

proof

thus { (N1 . i) where i is Element of N1 : i >= j1 } c= { (N2 . i) where i is Element of N2 : i >= j2 } :: according to XBOOLE_0:def 10 :: thesis: { (N2 . i) where i is Element of N2 : i >= j2 } c= { (N1 . i) where i is Element of N1 : i >= j1 }

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { (N1 . i) where i is Element of N1 : i >= j1 } or u in { (N2 . i) where i is Element of N2 : i >= j2 } )
assume u in { (N1 . i) where i is Element of N1 : i >= j1 } ; :: thesis: u in { (N2 . i) where i is Element of N2 : i >= j2 }
then consider i1 being Element of N1 such that
A4: u = N1 . i1 and
A5: j1 <= i1 ;
reconsider i2 = i1 as Element of N2 by A2;
N2 . i2 = u by A2, A4;
hence u in { (N2 . i) where i is Element of N2 : i >= j2 } by A2, A5; :: thesis: verum

end;

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { (N2 . i) where i is Element of N2 : i >= j2 } or u in { (N1 . i) where i is Element of N1 : i >= j1 } )
assume u in { (N2 . i) where i is Element of N2 : i >= j2 } ; :: thesis: u in { (N1 . i) where i is Element of N1 : i >= j1 }
then consider i2 being Element of N2 such that
A6: u = N2 . i2 and
A7: j2 <= i2 ;
reconsider i1 = i2 as Element of N1 by A2;
N1 . i1 = u by A2, A6;
hence u in { (N1 . i) where i is Element of N1 : i >= j1 } by A2, A7; :: thesis: verum

end;

then e = "/\" ( { (N2 . i) where i is Element of N2 : i >= j2 } ,R2) by A1, A3, Lm13;
hence e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } ; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } or e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } )
assume e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } ; :: thesis: e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum }
then consider j1 being Element of N2 such that
A8: e = "/\" ( { (N2 . i) where i is Element of N2 : i >= j1 } ,R2) ;
reconsider j2 = j1 as Element of N1 by A2;
set Y1 = { (N2 . i) where i is Element of N2 : i >= j1 } ;
set Y2 = { (N1 . i) where i is Element of N1 : i >= j2 } ;
{ (N2 . i) where i is Element of N2 : i >= j1 } = { (N1 . i) where i is Element of N1 : i >= j2 }

proof

thus { (N2 . i) where i is Element of N2 : i >= j1 } c= { (N1 . i) where i is Element of N1 : i >= j2 } :: according to XBOOLE_0:def 10 :: thesis: { (N1 . i) where i is Element of N1 : i >= j2 } c= { (N2 . i) where i is Element of N2 : i >= j1 }

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { (N2 . i) where i is Element of N2 : i >= j1 } or u in { (N1 . i) where i is Element of N1 : i >= j2 } )
assume u in { (N2 . i) where i is Element of N2 : i >= j1 } ; :: thesis: u in { (N1 . i) where i is Element of N1 : i >= j2 }
then consider i1 being Element of N2 such that
A9: u = N2 . i1 and
A10: j1 <= i1 ;
reconsider i2 = i1 as Element of N1 by A2;
N1 . i2 = u by A2, A9;
hence u in { (N1 . i) where i is Element of N1 : i >= j2 } by A2, A10; :: thesis: verum

end;

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { (N1 . i) where i is Element of N1 : i >= j2 } or u in { (N2 . i) where i is Element of N2 : i >= j1 } )
assume u in { (N1 . i) where i is Element of N1 : i >= j2 } ; :: thesis: u in { (N2 . i) where i is Element of N2 : i >= j1 }
then consider i2 being Element of N1 such that
A11: u = N1 . i2 and
A12: j2 <= i2 ;
reconsider i1 = i2 as Element of N2 by A2;
N2 . i1 = u by A2, A11;
hence u in { (N2 . i) where i is Element of N2 : i >= j1 } by A2, A12; :: thesis: verum

end;

then e = "/\" ( { (N1 . i) where i is Element of N1 : i >= j2 } ,R1) by A1, A8, Lm13;
hence e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } ; :: thesis: verum

end;

hence lim_inf N1 = lim_inf N2 by A1, Lm12; :: thesis: verum