let L be non empty reflexive RelStr ; :: thesis:
let x be Element of L; :: thesis:
set X = {x};

hereby :: according to WAYBEL_0:def 1 :: thesis:

let z, y be Element of L; :: thesis:
assume that
A1: z in {x} and
A2: y in {x} ; :: thesis:
take x = x; :: thesis:
thus ( x in {x} & z <= x & y <= x ) by A1, A2, TARSKI:def 1; :: thesis:

end;

hereby :: according to WAYBEL_0:def 2 :: thesis:

let z, y be Element of L; :: thesis:
assume that
A3: z in {x} and
A4: y in {x} ; :: thesis:
take x = x; :: thesis:
thus ( x in {x} & x <= z & x <= y ) by A3, A4, TARSKI:def 1; :: thesis:

end;