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
( a is_less_than X iff a9 is_less_than X )

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
( a is_less_than X iff a9 is_less_than X )

let X be Subset of L9; :: thesis: for a being Element of L
for a9 being Element of L9 st a = a9 holds
( a is_less_than X iff a9 is_less_than X )

let a be Element of L; :: thesis: for a9 being Element of L9 st a = a9 holds
( a is_less_than X iff a9 is_less_than X )

let a9 be Element of L9; :: thesis: ( a = a9 implies ( a is_less_than X iff a9 is_less_than X ) )
assume A1: a = a9 ; :: thesis: ( a is_less_than X iff a9 is_less_than X )
thus ( a is_less_than X implies a9 is_less_than X ) :: thesis: ( a9 is_less_than X implies a is_less_than X )
proof
assume A2: a is_less_than X ; :: thesis: a9 is_less_than X
now :: thesis: for q9 being Element of L9 st q9 in X holds
a9 [= q9
let q9 be Element of L9; :: thesis: ( q9 in X implies a9 [= q9 )
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: a9 [= q9
then A3: a [= q by A2;
a9 "/\" q9 = a "/\" q by
.= a9 by ;
hence a9 [= q9 by LATTICES:4; :: thesis: verum
end;
hence a9 is_less_than X ; :: thesis: verum
end;
thus ( a9 is_less_than X implies a is_less_than X ) :: thesis: verum
proof
assume A4: a9 is_less_than X ; :: thesis:
now :: thesis: for q being Element of L st q in X holds
a [= q
let q be Element of L; :: thesis: ( q in X implies a [= q )
assume A5: q in X ; :: thesis: a [= q
then reconsider q9 = q as Element of L9 ;
A6: a9 [= q9 by A4, A5;
a "/\" q = a9 "/\" q9 by
.= a by ;
hence a [= q by LATTICES:4; :: thesis: verum
end;
hence a is_less_than X ; :: thesis: verum
end;