let x, y be Element of T; :: according to WAYBEL_0:def 19 :: thesis: ( not x in A ` or not y <= x or y in A ` )
assume that
A1: x in A ` and
A2: y <= x ; :: thesis: y in A `
not x in A by A1, XBOOLE_0:def 5;
then not y in A by A2, WAYBEL_0:def 20;
hence y in A ` by XBOOLE_0:def 5; :: thesis: verum