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

proof

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

now :: thesis: for q9 being Element of L9 st q9 in X holds
q9 [= a9

let q9 be Element of L9; :: thesis: ( q9 in X implies q9 [= a9 )
the carrier of L9 c= the carrier of L by NAT_LAT:def 12;
then reconsider q = q9 as Element of L ;
assume q9 in X ; :: thesis: q9 [= a9
then A3: q [= a by A2;
q9 "/\" a9 = q "/\" a by A1, Th11
.= q9 by A3, LATTICES:4 ;
hence q9 [= a9 by LATTICES:4; :: thesis: verum

end;

hence X is_less_than a9 ; :: thesis: verum

end;

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

proof

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

now :: thesis: for q being Element of L st q in X holds
q [= a

let q be Element of L; :: thesis: ( q in X implies q [= a )
assume A5: q in X ; :: thesis: q [= a
then reconsider q9 = q as Element of L9 ;
A6: q9 [= a9 by A4, A5;
q "/\" a = q9 "/\" a9 by A1, Th11
.= q by A6, LATTICES:4 ;
hence q [= a by LATTICES:4; :: thesis: verum

end;

hence X is_less_than a ; :: thesis: verum

end;