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 )

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

thus
( a9 is_less_than X implies a is_less_than X )
:: thesis: verum
assume A2:
a is_less_than X
; :: thesis: a9 is_less_than X

end;now :: thesis: for q9 being Element of L9 st q9 in X holds

a9 [= q9

hence
a9 is_less_than X
; :: thesis: veruma9 [= 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 A1, Th11

.= a9 by A1, A3, LATTICES:4 ;

hence a9 [= q9 by LATTICES:4; :: thesis: verum

end;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 A1, Th11

.= a9 by A1, A3, LATTICES:4 ;

hence a9 [= q9 by LATTICES:4; :: thesis: verum

proof

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

end;now :: thesis: for q being Element of L st q in X holds

a [= q

hence
a is_less_than X
; :: thesis: veruma [= 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 A1, Th11

.= a by A1, A6, LATTICES:4 ;

hence a [= q by LATTICES:4; :: thesis: verum

end;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 A1, Th11

.= a by A1, A6, LATTICES:4 ;

hence a [= q by LATTICES:4; :: thesis: verum