( x <=> y = FALSE or x <=> y = TRUE ) by XBOOLEAN:def 3;
hence x <=> y is Element of BOOLEAN ; :: thesis: verum