thus types A is lower :: thesis: types A is directed

proof

let x, y be Element of T; :: according to WAYBEL_0:def 19 :: thesis: ( not x in types A or not y <= x or y in types A )
assume that
A1: x in types A and
A2: y <= x ; :: thesis: y in types A

now :: thesis: for a being adjective of T st a in A holds
y in types a

let a be adjective of T; :: thesis: ( a in A implies y in types a )
assume a in A ; :: thesis: y in types a
then x in types a by A1, Def13;
then A3: a in adjs x by Th13;
adjs x c= adjs y by A2, Th10;
hence y in types a by A3, Th13; :: thesis: verum

end;

hence y in types A by Def13; :: thesis: verum

end;

let x, y be Element of T; :: according to WAYBEL_0:def 1 :: thesis: ( not x in types A or not y in types A or ex b₁ being Element of the carrier of T st
( b₁ in types A & x <= b₁ & y <= b₁ ) )
assume that
A4: x in types A and
A5: y in types A ; :: thesis: ex b₁ being Element of the carrier of T st
( b₁ in types A & x <= b₁ & y <= b₁ )
take x "\/" y ; :: thesis: ( x "\/" y in types A & x <= x "\/" y & y <= x "\/" y )

now :: thesis: for a being adjective of T st a in A holds
x "\/" y in types a

let a be adjective of T; :: thesis: ( a in A implies x "\/" y in types a )
assume A6: a in A ; :: thesis: x "\/" y in types a
then y in types a by A5, Def13;
then A7: a in adjs y by Th13;
x in types a by A4, A6, Def13;
then a in adjs x by Th13;
then a in (adjs x) /\ (adjs y) by A7, XBOOLE_0:def 4;
then a in adjs (x "\/" y) by Def11;
hence x "\/" y in types a by Th13; :: thesis: verum

end;

hence ( x "\/" y in types A & x <= x "\/" y & y <= x "\/" y ) by Def13, YELLOW_0:22; :: thesis: verum