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
A3: adjs x c= adjs y by A2, Th10;
a in adjs x by A1, Th13;
hence y in types a by A3, Th13; :: 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 )
A6: a in adjs y by A5, Th13;
a in adjs x by A4, Th13;
then a in (adjs x) /\ (adjs y) by A6, XBOOLE_0:def 4;
then a in adjs (x "\/" y) by Def11;
hence ( x "\/" y in types a & x <= x "\/" y & y <= x "\/" y ) by Th13, YELLOW_0:22; :: thesis: verum