let L be Lattice; :: thesis: for L' being SubLattice of L
for X being Subset of L'
for a being Element of L
for a' being Element of L' st a = a' holds
( X is_less_than a iff X is_less_than a' )
let L' be SubLattice of L; :: thesis: for X being Subset of L'
for a being Element of L
for a' being Element of L' st a = a' holds
( X is_less_than a iff X is_less_than a' )
let X be Subset of L'; :: thesis: for a being Element of L
for a' being Element of L' st a = a' holds
( X is_less_than a iff X is_less_than a' )
let a be Element of L; :: thesis: for a' being Element of L' st a = a' holds
( X is_less_than a iff X is_less_than a' )
let a' be Element of L'; :: thesis: ( a = a' implies ( X is_less_than a iff X is_less_than a' ) )
assume A1: a = a' ; :: thesis: ( X is_less_than a iff X is_less_than a' )
thus ( X is_less_than a implies X is_less_than a' ) :: thesis: ( X is_less_than a' implies X is_less_than a )

proof

assume A2: X is_less_than a ; :: thesis: X is_less_than a'

now

let q' be Element of L'; :: thesis: ( q' in X implies q' [= a' )
the carrier of L' c= the carrier of L by NAT_LAT:def 16;
then reconsider q = q' as Element of L by TARSKI:def 3;
assume q' in X ; :: thesis: q' [= a'
then A3: q [= a by A2, LATTICE3:def 17;
q' "/\" a' = q "/\" a by A1, Th12
.= q' by A3, LATTICES:21 ;
hence q' [= a' by LATTICES:21; :: thesis: verum

end;

hence X is_less_than a' by LATTICE3:def 17; :: thesis: verum

end;

thus ( X is_less_than a' implies X is_less_than a ) :: thesis: verum

proof

assume A4: X is_less_than a' ; :: thesis: X is_less_than a

now

let q be Element of L; :: thesis: ( q in X implies q [= a )
assume A5: q in X ; :: thesis: q [= a
then reconsider q' = q as Element of L' ;
A6: q' [= a' by A4, A5, LATTICE3:def 17;
q "/\" a = q' "/\" a' by A1, Th12
.= q by A6, LATTICES:21 ;
hence q [= a by LATTICES:21; :: thesis: verum

end;

hence X is_less_than a by LATTICE3:def 17; :: thesis: verum

end;